 \documentclass[11pt,compress]{beamer}
% \documentclass[11pt,compress,handout]{beamer}

%\usepackage{pgfpages}
%\setbeameroption{show notes}
%\setbeameroption{show notes on second screen=right}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsthm, amsfonts} 
\usepackage{mathpartir}
\usepackage{textcomp}
\usepackage{stmaryrd}
\usepackage{myproof}
%\usepackage{evolvablemacro}

\newcommand{\nopen}[2]{\mathsf{open}\,#1\,(#2)}
\newcommand{\nopenr}[2]{\mathsf{request}\,#1\,(#2)}
\newcommand{\nopena}[2]{\mathsf{accept}\,#1\,(#2)}
\newcommand{\open}[1]{\mathsf{open}(#1)}
\newcommand{\close}[1]{\mathsf{close}\langle#1\rangle}

\newcommand{\restr}[2]{(\nu #1 )#2}

\newcommand{\ifte}[3]{\mathsf{if}~ #1 ~\mathsf{then}~ #2 ~\mathsf{ else }~#3}

\newcommand{\branch}[2]{#1\triangleright \{#2\}}
\newcommand{\select}[2]{#1\triangleleft #2}

\newcommand{\rec}[2]{\mathrm{rec} (#1).#2}
\newcommand{\qua}{\ensuremath{\mathsf{q}}}  % 
\newcommand{\sepr}{ \  \mid \ }
\newcommand{\updated}[5]{{#1}^{#3}_{#4}\{#5(\mathsf{#2})\} } % a{P}
\newcommand{\inC}[2]{#1(#2)}  % output
\newcommand{\outC}[2]{\overline{#1}\langle #2 \rangle}  % output
\newcommand{\outCi}[1]{\overline{#1}}  % output
\newcommand{\throw}[2]{{#1}!(#2)}  % throw
\newcommand{\catch}[2]{{#1}?(#2)}  % throw
\newcommand{\componente}[3]{#1^#2 [#3]   }  %a^n[P]
\newcommand{\component}[2]{#1 [#2]   } 
%\newcommand{\componente}[2]{#1[#2]   }  %a^n[P]
\newcommand{\updates}[3]{{#1}\{#2(#3)\} } % a{P}
\newcommand{\update}[2]{\widetilde{#1}\{#2\} }
\newcommand{\updaten}[2]{{#1}\{#2\} } % a{P}
\def\sub#1#2{\{\raisebox{.5ex}{\small$#1$}\! / \mbox{\small$#2$}\}} %substitution
\newcommand{\intf}[1]{\mathcal{I}_{[#1]}}
\newcommand{\compat}{\ensuremath{\asymp}}  % 
%\newcommand{\nm}[1]{\ensuremath{\mathsf{#1}}}
% \newcommand{\nmu}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\componentbig}[2]{#1 \bigg[ #2 \bigg]   }  %a[P]
\newcommand{\componentbbig}[2]{#1 \big[ #2 \big]   }  %a[P]
\newcommand{\mupdate}[4]{{#1}\big\{#2\big\}} % a{P}
\newcommand{\capab}{\tau}

\newcommand{\evol}[1]{\ensuremath{\mathcal{E}^{\mathtt{#1}}}\xspace}
\newcommand{\evold}[1]{\ensuremath{\mathcal{E}_d^{\mathtt{#1}}}\xspace}
\newcommand{\evols}[1]{\ensuremath{\mathcal{E}_s^{\mathtt{#1}}}\xspace}
\newcommand{\OG}{\ensuremath{\mathsf{\mathbf{BA}}}\xspace} % bounded adaptation
\newcommand{\LG}{\ensuremath{\mathsf{\mathbf{EA}}}\xspace} % eventual adaptation

\newcommand{\env}[2]{#1 \,;\, #2}
\newcommand{\type}[2]{#1 \, ; \, #2}
\newcommand{\judgement}[5]{\env{#1}{#2} \vdash #3 :: \type{#4}{#5}}
%\newcommand{\judgebis}[3]{#1 \vdash #2 :: #3}
\newcommand{\judgebis}[3]{#1 \vdash #2\triangleright #3}





%\usepackage{japerez}
% Davides's macro
\usepackage{davidemacro}
%\usepackage{evolvablemacro}

%\usepackage[latin1]{inputenc}
%\usepackage[T1]{fontenc}
%\usepackage{pgfpages}

%\usepackage{times}
\usepackage{xspace}

\usepackage[english]{babel}
\usepackage{url}

\usepackage{wrapfig}

\hypersetup{%
	pdftitle={Adaptable Processes},%
	pdfauthor={Jorge A. Perez},%
	pdfsubject={},%
	pdfkeywords={process calculi, concurrency}%
}

\usepackage{color}
%\newcommand{\emphcolor}[1]{\textcolor{orange}{#1}\xspace}
\newcommand{\emphcolor}[1]{\textcolor{purple}{#1}\xspace}
\newcommand{\emphcolorb}[1]{\textcolor{blue}{#1}\xspace}
\newcommand{\emphcolorm}[1]{\textcolor{magenta}{#1}\xspace}

\newcommand{\whitecolor}[1]{\textcolor{white}{#1}\xspace}
\newcommand{\hidecolor}[1]{\textcolor{darkgray}{#1}\xspace}
\newcommand{\olivecolor}[1]{\textcolor{olive}{#1}\xspace}

%red, gray,
%orange,
%green, white, pink,
%blue, darkgray,
%cyan,	magenta,	yellow,	black, lightgray,	brown,	lime,	olive,
%purple,

\newcommand{\tealtext}[1]{\textcolor{teal}{#1}\xspace}

\newcommand{\str}[1]{\structure{#1}}


%\def\sub#1#2{\{\raisebox{.5ex}{\small$#1$}\! / \mbox{\small$#2$}\}}
%\newcommand{\til}[1]{\widetilde{#1}}
%\newcommand{\update}[2]{\til{#1}\{#2\} } 
%\newcommand{\component}[2]{#1 [#2]   }  %a[P]
%\newcommand{\outC}[1]{\overline{#1}}      % CCS  output

\newcommand{\bi}{\begin{itemize}}
\newcommand{\ei}{\end{itemize}}
\newcommand{\be}{\begin{enumerate}}
\newcommand{\ee}{\end{enumerate}}
\newcommand{\bbl}[1]{\begin{block}{#1}}
\newcommand{\ebl}{\end{block}}

\newcommand{\notas}[1]{\hidecolor{{\footnotesize {[#1]}}}}
\newcommand{\notass}[1]{\hidecolor{{\footnotesize {#1}}}}

% Context
\newcommand{\ol}{\langle\!\langle}
\newcommand{\cl}{\rangle\!\rangle}
\newcommand{\hl}[1]{\ol #1 \cl}
\newcommand{\fillcon}[2]{\ensuremath{#1\hl{#2}}}

\newcommand{\pired}{\longrightarrow}
\newcommand{\arro}[1]{\xrightarrow[]{#1}}

\newcommand{\rulename}[1]{\textsc{(#1)}}

\newcommand{\nm}[1]{\ensuremath{\mathsf{#1}}}
 \newcommand{\nmu}[1]{\ensuremath{\mathtt{#1}}}
 \newcommand{\midef}{\ensuremath{\stackrel{\mathsf{def}}{=}}}



%\newcommand{\str}[1]{\structure{#1}}
\newcommand{\fkspc}{{\tiny \ }\\}


\title[Session Types for Dynamically Evolvable Communicating Systems]{Adaptable Processes and \\ Runtime Adaptation for Session Types}
\author[Cinzia Di Giusto and Jorge A. P\'erez]{Jorge A. P\'erez \\ {\small (joint works with Mario Bravetti, Cinzia Di Giusto, and Gianluigi Zavattaro)}}
%\date[June 8, 2011]{GLOSS Seminar, FCUL - September 15, 2011}
\date{UniBo -- May 13, 2013}
  
\institute{\normalsize{CITI - DI, Universidade NOVA de Lisboa}}

\setbeamertemplate{navigation symbols}{} 

\usecolortheme{default}
%\useoutertheme{progressbar}
%\useinnertheme{progressbar}
%\usefonttheme{progressbar}

\usepackage{setspace}

\newcommand{\putat}[3]{\begin{picture}(0,0)(0,0)\put(#1,#2){#3}\end{picture}}



\AtBeginSection[]
{
  \begin{frame}<beamer>
    \frametitle{Outline}
    \tableofcontents[currentsection]
  \end{frame}
}



\begin{document}



\begin{frame}
%\progressbaroptions{titlepage=normal}
	
 \titlepage
\end{frame}




\section{Context and Motivation}

\frame{
\frametitle{Adaptation and Evolution}
Modern software systems and apps require \\
to \emphcolor{adapt} to their environment and \str{evolve} accordingly:
\bi
\item Enforce new requirements; enhance reliability
\item Implement maintenance or recovery policies
\item React to unexpected circumstances \\ (such as errors and user demand peaks) \pause
\ei
\notas{All of the above: as transparently as possible} \pause

\bigskip

A complex issue; many possible perspectives:
\bi
\item System infrastructures \notas{e.g. scaling in cloud computing}
\item Software architectures/paradigms \\ \notas{e.g. aspect-oriented and context-aware programming}
\item \str{Programming languages and models} \\ E.g. constructs for exceptions, compensations, reversibility.
\ei
}

\frame{
\frametitle{Fault tolerance in Erlang: Supervisors}
\bi
\item Programs conceptually divided into \str{workers} and \str{supervisors}
\item Workers perform actual computational behavior %\\ \notas{i.e., asynchronous message-passing programs}
\item Supervisors are \str{adaptation mechanisms}: they monitor a worker's behavior, enabling restarting actions if needed
\ei
\vspace{-5mm}\begin{center}
\includegraphics[height=40mm]{suptree}
\end{center}
\vspace{-5mm}Remarkably:
\bi
\item Hierarchical structure brings organization and flexibility %(e.g., a worker's supervisor may be ifself supervised)
\item Relative independence between supervisors and workers
\ei
}


\frame{
\frametitle{Adaptation and Evolution in Models of Concurrency}

Widely studied models for concurrency are \str{not suited} to account for \emphcolorm{complex} forms of evolution/reconfiguration
\pause


\bi
\item Suspend, replace, modify portions of the system at runtime
\ei

\bigskip \pause
In particular, in models of communicating processes:
\bi
\item Name passing is useful but only at a local (low) level
\item Global, atomic reconfiguration is difficult to express
\item Resulting models are contrived and/or hard to reason about
\ei

\bigskip

Frameworks for disciplined communications (such as session types)
build upon the above, but currently 
incorporate only limited forms of evolution/reconfiguration.

}

\frame{
\frametitle{This Talk}


\begin{block}{1. Adaptable processes} Extend models of communicating processes with 
\bi
\item \str{Located processes} \\ Distinguished sites in which behavior resides 
\item \str{Update processes} \\ Adaptation functions which act on located processes
\ei
Good knowledge on decidability and verification results
\end{block}

\bigskip

\begin{block}{2. An integration of adaptable processes and session types}
\bi
\item %Ongoing work. 
Typed processes with built-in adaptation mechanisms 
\item Session delegation enhanced with runtime adaptation
\item Updates depend on a (very basic) notion of interfaces
\item Consistency: reconfiguration doesn't disrupt open sessions
\ei
\end{block}
}

%\frame{
%\frametitle{This Work: Adaptation for Communicating Processes}
%
%
%More flexible and open models of communicating systems by integrating rich and flexible
%\str{built-in adaptation mechanisms} 
%
%\smallskip
%
%\begin{block}{Context}
%Interacting partners (expressed as $\pi$-calculus processes) which execute
% communication protocols (enforced via session types)
%\end{block}
%%\vspace{-2mm}
%\begin{block}{Goals}
%\bi
%\item \str{Integration of concerns:} Enforce communication correctness while admitting useful forms of runtime reconfiguration
%\item \str{Conservativity:} Stay as close as possible to ``usual'' session-based frameworks  
%\ei
%\end{block}
%%\vspace{-2mm}
%\begin{block}{Main challenge}
%Harmonize communication behavior and reconfiguration actions
%\end{block}
%}
%
%
%\frame{
%\frametitle{Our Choices} 
%A synchronous $\pi$-calculus with \str{adaptable processes}
%\bi
%\item \str{Located processes} \\ Distinguished sites in which behavior resides 
%\item \str{Update processes} \\ Adaptation functions which act on located processes
%\ei
%
%\bigskip
%
%We build upon \emphcolorm{safe sessions} for Ambients \notas{Garralda et al.-PPDP'06}:
%\bi
%\item Binary session types \str{with delegation}
%\item Processes spread over arbitrary (but explicit) domains
%\item Prioritize communication over reconfiguration
%\item Updates dependant on (basic) notions of interfaces/contracts %\\ \notas{used to enable/control reconfiguration}
%\ei
%
%\begin{block}{Results}
%\bi
%\item Session fidelity: Session types are respected along execution
%\item Consistency: Update actions do not interrupt  active sections
%\ei
%\end{block}
%}



\section{Adaptable Processes}

\begin{frame}
\frametitle{Adaptable processes}
A process calculi approach to evolvable systems
%\pause
\begin{itemize}
  \item Provide \emphcolor{direct control} on process execution 
  \item Processes can be stopped, restarted, relocated, at runtime 
  \item A form of \emphcolor{higher-order} process communication
 % \item 
\end{itemize}
\smallskip
Defined for a fragment of CCS; the concept scales up to other calculi

%\pause
%\begin{block}{Our proposal}
%\begin{enumerate}
%\item A \emphcolor{process calculus} of adaptable processes, called \emphcolorb{\evol{}} %\pause
%\item \emphcolor{Verification problems} for evolvable systems defined in \evol{} %\pause
%\item \emphcolor{(Un)decidability results} for such problems
%\end{enumerate}
%\end{block}
%\pause In \str{this talk} I will  focus mainly on (1) and (2) 
\end{frame}

\begin{frame}
\frametitle{A calculus for adaptable processes }

\begin{block}{Syntax}
\visible<1,2,3,4>CCS without restriction \invisible<1>{plus \emphcolor{located processes}\\}\invisible<1,2>{ and \emphcolorb{update prefixes}:}
$$
\begin{array}{ll}
P        ::=& \sum_{i \in I} \pi_i.P_i   \, \midd \, 
          P \parallel P  \, \midd \, ! \pi.P \, \invisible<1>{\midd \, \emphcolor{\component{a}{P}}}\\ \\
\pi   ::=&  a \, \midd \, \outCi{a} \invisible<1,2>{\, \midd \, \emphcolorb{\update{a}{U}}}
\end{array}
$$
\invisible<1,2,3>{where 
\begin{itemize}
\item $\component{a}{P}$ is the \emphcolor{adaptable process} $P$ \emphcolor{located at} name $a$
\item $U$ is a \emphcolorb{context}, with zero or more \emphcolorb{holes}, denoted $\bullet$
\end{itemize}}
\end{block}

\end{frame}








\begin{frame}
\frametitle{A calculus for adaptable processes}

\begin{block}{Operational Semantics: Intutions}
\begin{itemize}
\item Localities are \emphcolor{transparent}:
$$
 \rightinfer
 			{\component{a}{P} \xrightarrow{~\alpha~}  \component{a}{P'}}
 			{P \xrightarrow{~\alpha~} P'} 
			$$
			
\item Reconfiguration via \emphcolor{interaction}  with update prefixes:
$$
\component{a}{P} \parallel \update{a}{U}.Q \xrightarrow{~\tau~} \fillcon{U}{P} \parallel Q
$$
%\pause 
\hspace{-6mm}
\small{[$\fillcon{U}{P}$ is the \emphcolor{process} obtained by filling in the holes in $U$ with $P$]}
%\item An update replaces an adaptable process with a
%new process filled with the process currently
%active in the updated location
%
%\end{itemize}
%
%metti sintassi di techrep
% $$
%\begin{array}{c}
% \component{a}{P} \xrightarrow{~\component{a}{P}~}  \star
%\qquad 
%\rightinfer
%			{P_1 \parallel P_2 \xrightarrow{~\tau~} P_1'\sub{ U \sub{Q}{\bullet}  }{\star} \parallel P_2'}
%			{P_1 \xrightarrow{~\component{a}{Q}~} P_1' \qquad P_2 \xrightarrow{~\update{a}{U}~} P_2'}
%\end{array}
%$$
\end{itemize}
\end{block}

\end{frame}

\frame{
\frametitle{A calculus for adaptable processes}
%\vspace{-4mm}
\begin{block}{Operational Semantics: LTS}
%\vspace{-6mm}
%A Labeled Transition System (LTS) which extends that of C
{\footnotesize
$$
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
%\fbox{\inferrule[\rulename{Comp}]{}{\component{a}{P} \arro{~\component{a}{P}~}  \star}}
%\qquad 
%  \mathrm{\textsc{Upd}}~~~\update{a}{P_1}.P_2 \arro{\update{a}{P_1}}  P_2
%$$
%$$
\hidecolor{\inferrule[]{}{\sum_{i\in I} \alpha_i.P_i \arro{~\alpha_i~}  P_i } }
%\rightinfer	[\textsc{Rec}]
 %			{rec \,X.P \arro{\alpha} P}
 %			{P\sub{rec \, X.P}{X} \arro{\alpha} P'}
 %\quad
\qquad
\hidecolor{\inferrule[]{}{!\alpha.P \arro{~\alpha~}  P \parallel !\alpha.P }}
$$
$$
%\fbox{\inferrule[\rulename{Loc}]{P \arro{~\alpha~} P'}{\component{a}{P} \arro{~\alpha~}  \component{a}{P'}}}
%\quad 
\hidecolor{\inferrule[]{P_1 \arro{~\alpha~} P_1'}{P_1 \parallel P_2 \arro{~\alpha~} P'_1 \parallel P_2}	}
\quad
\hidecolor{\inferrule[]{P_1 \arro{~a~} P_1' \andalso P_2 \arro{~\outCi{a}~} P'_2}{P_1 \parallel P_2 \arro{~\tau~}  P'_1 \parallel P'_2}}
$$
}
\pause
$$
\hspace{-8mm}
\fbox{
\inferrule[]{}{\component{a}{P} \arro{~\component{a}{P}~}  \star}
\quad  
\inferrule[]{P \arro{~\alpha~} P'}{\component{a}{P} \arro{~\alpha~}  \component{a}{P'}}
\quad~~
\inferrule[]{P_1 \arro{~\component{a}{\emphcolor{Q}}~} P_1'\andalso P_2 \arro{~\update{a}{\emphcolorb{U}}~} P_2' }{P_1 \parallel P_2 \arro{~\tau~} P_1'\sub{ \fillcon{\emphcolorb{U}}{\emphcolor{Q}}  }{\star} \parallel P_2'}~}
$$
\\ 
\hidecolor{[Reduction $\pired$ is defined as $\arro{~\tau~}$]}
\end{block}
}



\frame{
\frametitle{Some evolvability patterns}
\begin{description}
\item<1-3>[Replacement] $$\quad \component{a}{\emphcolor{Q}} \parallel \update{a}{\str{\component{a}{R}}}.S \pired \str{\component{a}{R}} \parallel S  ~~(\bullet \not \in R)$$ 
\item<2-3>[Destroyer]$$\quad \component{a}{\emphcolor{Q}} \parallel \update{a}{\str{R}}.S \pired \str{R} \parallel S  ~~(\bullet \not \in R)$$ 
\item<3>[Plug-in] $$\component{a}{\emphcolor{Q}} \parallel \update{a}{\str{\component{a}{c{.}\bullet +R}}}.\nil \pired \str{\component{a}{c{.}\emphcolor{Q} +\fillcon{R}{\emphcolor{Q}}}} \parallel \nil$$ 
\end{description}
}

\frame{
\frametitle{Some evolvability patterns}
\begin{description}
\item<1-3>[Renaming] $$\componentbbig{m}{\component{a}{\emphcolor{Q}}} \parallel \componentbbig{n}{\update{a}{\str{\component{b}{\bullet}}}.S} \pired \componentbbig{m}{\str{\component{b}{\emphcolor{Q}}}}\parallel \componentbbig{n}{S}$$
\item<2-3>[Backup] $$\component{a}{\emphcolor{Q}} \parallel \update{a}{\str{\component{a}{\bullet}} \parallel \str{\component{b}{\bullet}}}.S \pired \str{\component{a}{\emphcolor{Q}}} \parallel \str{\component{b}{\emphcolor{Q}}} \parallel S$$
\item<3>[Deep update] $$\hspace{-55pt}\componentbbig{a}{Q \parallel \component{b}{R \parallel \emphcolor{\component{c}{S_{1}}}\, }\, } \parallel \update{c}{\str{\component{d}{S_{2}}}}.\nil \pired \componentbbig{a}{Q \parallel \componentbbig{b}{R \parallel \str{\component{d}{S_{2}}}\, }\, } \parallel \nil $$
\end{description}
}



\frame{
\frametitle{Supervisors as Adaptable Processes (1)}

\bi
\item Let $\component{l_1}{P_1}, \ldots, \component{l_n}{P_n}$ be definitions of located services. \\
Each service $P_j$ has a unique failure signal $\outCi{f_j}$
\item Let $S_{\mathtt{one}}^{\,\til{l}, \, \til{f}}(P_1, \ldots, P_n)$ be a \str{one-supervisor} defined as
$$
\prod_{i \in \{1,\ldots, n\}} f_i.\update{l_i}{\component{l_i}{P_i}}
$$
That is, local failure entails local adaptation/restart. \pause
%and so it restarts a single $P_k$ in case of failure---all the other process remain unchanged
\item Let $S_{\mathtt{all}}^{\,\til{l}, \, \til{f}}(P_1, \ldots, P_n)$ be an \str{all-supervisor} defined as
$$
\sum_{i \in \{1,\ldots, n\}} f_i. \prod_{j \in \{1,\ldots, n\}}\update{l_j}{\component{l_j}{P_j}}
$$
%and so it restarts a single $P_k$ in case of failure---all the other process remain unchanged
That is, local failure entails global adaptation/restart.
\ei

}


\frame{
\frametitle{Supervisors as Adaptable Processes (2)}

\bi
%\item Let $\component{l_1}{P_1}, \ldots, \component{l_n}{P_n}$ be a finite series of service declarations. \\ Each $P_j$ has a failure signal $\outCi{f_j}$

\item Using nested locations, we model a supervision tree  as %follows:
$$
Tree_{\mathtt{all}} = \componentbig{t}{\componentbbig{s}{S_{\mathtt{all}}^{\,\til{l}, \, \til{f}}(P_1, \ldots, P_n)} \parallel \component{l_1}{Q_1} \parallel \ldots \parallel \component{l_n}{Q_n}}
$$
(and similarly for $ Tree_{\mathtt{one}}$)
\item The supervisor itself may be adapted by an update on $s$:
$$
Tree_{\mathtt{all}} \parallel \update{s}{\componentbbig{s}{S_{\mathtt{all}}^{\,\til{l}, \, \til{f}}(P_1, \ldots, P_n)}} \pired Tree_{\mathtt{one}}
$$

\ei
}


%\frame{
%\frametitle{A first example}
%
%A basic client-server scenario:  
%\begin{eqnarray*}
%C & = & \componentbbig{client}{\component{run}{P} \parallel \outC{upd}.Q} \\
%S & = & \componentbbig{server}{upd.\update{run}{\component{run}{R \parallel old.\bullet}}.S} 
%\end{eqnarray*}
%
%\pause
%
%We then have two interactions, first on \emphcolor{$upd$} then on \emphcolor{$run$}:
%\begin{align*}
%%P & \componentbbig{client}{\component{run}{P} \parallel \outC{upd}.C} \parallel \componentbbig{server}{upd.\update{run}{\component{run}{Q \parallel old.\bullet}}.S} \\ 
%C \parallel S \pired ~ & \componentbbig{client}{\component{run}{\emphcolor{P}} \parallel  Q} \parallel \componentbbig{server}{\update{run}{\str{\component{run}{R \parallel old.\bullet}}}.S} \\ 
%\pired ~ & \componentbbig{client}{\str{\component{run}{R \parallel old.\emphcolor{P}}} \parallel Q} \parallel \componentbbig{server}{S}
%\end{align*}
%
%}

\frame{
\frametitle{Decidability and Verification Results for APs}


We investigated \LG/\OG, 
 two \str{adaptation problems} over adaptable processes. 
 Let $e$ be a designated signal. 

%Both specify a future correct state of the workflow:
\begin{itemize}
\item While \LG says that $e$ will  \emphcolor{eventually} disappear...
\item \OG says $e$ will disappear \emphcolor{within a certain time bound}.
\end{itemize}

\bigskip 
A set of (un)decidability results for \LG/\OG [Log. Meth. CS'12]:
\begin{itemize}

\item Structural and behavioral variants of the calculus

\item Undecidability via encodings of \emphcolorb{two-counter machines} %\pause

\item Decidability via \emphcolorb{well-structured transition systems} and \emphcolorb{Petri nets reductions}

\end{itemize} 

\bigskip

These results were generalized to properties of a small temporal logic [ISOLA'12].

}


%\frame{
%\frametitle{Summary of (un)decidability results}
%
%{\small
%\begin{table}
%%\begin{center}
%%\hspace{-8mm}
%\begin{tabular}{c|c|c}
%		& \evold{} -- Dynamic Topology & \evols{} -- Static Topology \\
%\hline \hline
%\evol{1}	&~ \OG undec ~/~\LG undec ~& ~\OG undec~/~\LG undec~\\
%\hline
%\evol{2}	& ~ \OG \emphcolor{decidable}~/~\LG undec ~ & ~ \OG \emphcolor{decidable}~/~\LG undec \\
%\hline
%\evol{3}	& ~ \OG \emphcolor{decidable}~/~\LG \str{undec} ~ & \OG~\emphcolor{decidable}~/~\LG \emphcolor{decidable} 
%\end{tabular}
%%\end{center}
%\end{table}
%}
%
%\pause 
%
%\begin{itemize}
%\item Undecidability via encodings of \emphcolorb{two-counter machines} \pause
%
%\item Decidability of $\OG$ via \emphcolorb{well-structured transition systems} \pause 
%
%\item Decidability of $\LG$ via  a reduction to a \emphcolorb{place boundedness}, a decidable problem in Petri nets
%
%\end{itemize} 
%
%}


\section{A Session Language with APs}

\frame{
\frametitle{Session Types for Adaptable Processes in One Slide}

\begin{block}{Key Ideas:}
\bi
\item A synchronous $\pi$  with adaptable and update processes
\item Key idea: harmonize communication and adaptation actions
\item Consistency: adaptation does not disrupt communication
\ei
Ongoing work---a first attempt, building upon safe sessions for Ambients, presented at SAC'13. 
\end{block}

\bigskip
\pause

We wish to be conservative:
\bi
\item Types and judgements as usual, extended with an interface \\ (a sequence of declared services, attached to locations)
\item Keep track of open sessions at a given location
\item Allow updates only on locations without open sessions
\ei
%\end{block}

\bigskip

We can express:
\bi
\item Runtime update of service declarations / Service extension
\item Relocation of active processes
\ei
%\end{block}

}



\frame{
\frametitle{A Session Language with APs (Excerpt)}

%In a session-typed context, the two constructs are annotated:
$$
\begin{array}{lclr}
P \!\!& \!\!::=  
	& \!\!\! \nopenr{a}{x}.P  & \text{service request}	\\
	& \sepr & \!\!\! \nopena{a}{x}.P  & \text{service request}	 \\
	& \sepr & \!\!\!\outC{k}{\tilde{e}}.P & \text{data output}  \\
  	&\sepr &  \!\!\! \inC{k}{\tilde{x}}.P  & \text{data input} \\
	& \sepr & \!\!\!\throw{k}{k'}.P & \text{channel output} \\
    &\sepr &  \!\!\!\catch{k}{x}.P  & \text{channel input} \vspace{1mm}\\
	&\sepr& \!\!\!\componente{loc}{h}{P} ~~(h \geq 0)  & \text{\emphcolor{adaptable process}}\vspace{1mm} \\
% &   & \sepr & \!\!\! \mathsf{X}& \text{process variable} \\
	&\sepr& \!\!\!\updates{loc}{P}{X} & \text{\emphcolorb{update process}} \vspace{1mm}\\
%  	& \sepr & \!\!\!\ifte{e}{P}{Q} & \text{conditional}\\
%	    & \sepr & \!\!\! Y& \text{recursion variable}\\	 
%	& \sepr & \!\!\! \rec{Y{:}\Phi{\cdot}\Delta}{P}& \text{recursion}\\	
  	& \sepr & \!\!\! P \parallel P & \text{parallel}\\	 
%	&\sepr& \!\!\! \branch{c}{n_1:P_1, \ldots, n_k:P_k} & \text{branching}\\
%	&\sepr& \!\!\! \select{c}{n}.P & \text{selection}\\
		&\sepr& \!\!\! \close{k}.P & \text{close session}	\\
			&\sepr& \!\!\! \restr{u}{P}  & \text{name/channel hiding}	\\
			&\sepr& \!\!\! \mathbf{0}  & \text{inaction} %\\
%e	&::= & \!\!\! k &\text{constants} \\
%    & \sepr & \!\!\! e_1 + e_2 \sepr e_1 - e_2  \sepr \ldots & \text{operators}
\end{array} 
$$

%Key annotations:
\bi
%\item Association with session types is \emph{local}. %
\item $h$: the number of open sessions (end points) at a  location
%\item Explicit close construct. 
%\item  $\mathcal{I}$: an interface (set of declared sessions)
\ei
}


\frame{
\frametitle{A Session Language with Adaptable Processes (2)}

$C, D, E$~: transparent evaluation contexts ---nested locations.\\
$C^{+}$, $C^{-}$~: propagate changes in the annotations of locations in $C$.

$$
\begin{array}{c}
E\big[C[\nopenr{a}{x}.P] \parallel D[\nopena{a}{x}.Q]\big] \\
\pired  \\
 \restr{\kappa}{\big(E^{++}_{}\big[{C^{+}_{}[P\sub{\kappa^+}{x}] \parallel D^{+}_{}[Q\sub{\kappa^-}{x}]}\big]\big)} \vspace{8mm} \\
E\big[C[\throw{k}{k'}.P] \parallel D[\catch{k}{x}.Q]\big] \pired E\big[C^{-}[P] \parallel D^{+}[Q\sub{k}{x}]\big] 
 \vspace{8mm}\\
E\big[C[\componente{loc}{0}{Q}] \parallel D[\updates{loc}{P}{X}]\big]~~ 
%{\small \emphcolorb{(\text{with }\intf{Q} \compat\mathcal{I}_1)}} \\ 
\pired   
E_{}\big[C[P\sub{Q}{\mathsf{X}}] \parallel D[\nil]\big] \vspace{8mm} \\
E\big[C[\close{\kappa^+}.P] \parallel D[\close{\kappa^-}.Q]\big] \pired  E^{-}\big[C^{-}[P] \parallel D^{-}[Q]\big]
\end{array}
$$


%Observe:
%\bi
%%\item Session establishment enforces type duality %Location counters are increased. 
%\item Reconfiguration depends on interface compatibility, noted $\compat$
%\ei
}


\frame{
\frametitle{An Example}
%We may  abstract a workflow application as the following  process:
% $$
%  App ~\triangleq~ \componentbig{\nm{wfa}^0}{\, \componentbbig{\nm{we}^0}{\nmu{WE} \parallel \nm{W}_{1} \parallel \cdots \parallel \nm{W}_{k} \parallel \componente{\nm{\nm{wbl}}}{0}{\nmu{BL}}} \parallel \nmu{S}_{1} \parallel \cdots \parallel \nmu{S}_{j}\,}
% $$
% where the $i$-th workflow (two activities, located on names $\nm{r}$ and $\nm{t}$) is defined as:
Suppose a process 

 $$
%\nm{W}_{i} \triangleq \componentbig{\nm{w}_{i}^0}{\,  \nmu{WL}_{i} \parallel \prod_{j=1}^n  \component{\nm{a}_j}{0}{}{\nmu{P}_{j}}  \,}
\nm{W}_{i} \triangleq \componentbbig{\nm{w}_{i}^0}{\, Adapt_r \parallel  \componente{\nm{r}}{0}{\nmu{P}_{1}} \parallel  \componente{\nm{t}}{0}{\nmu{P}_{2}} \,}
$$
%Suppose that $\nm{W}_{i}$ has two activities only, : $\nm{W}_{i} \triangleq \componentbbig{\nm{w}_{i}^0}{\,  \nmu{WL}_{i} \parallel  \component{\nm{r}}{0}{}{\nmu{P}_{1}} \parallel  \component{\nm{t}}{0}{}{\nmu{P}_{2}} \,},$ 

where location $r$ defines a disciplined behavior: % (with type $\sigma$): %with  $\nmu{P}_1$ defined as
\begin{eqnarray*}
\nmu{P}_1 \!\!& \!\!\triangleq \!\!& \nopena{a}{s}.\inC{s}{u,p}.\select{s}{n_1.Q[s]}.\close{s} 
\end{eqnarray*}

%\bigskip

Suppose $Adapt_r$ is defined as: % for $\nm{W}_{i}$: 
%for location $\nm{r}_{}$.
\begin{eqnarray*}
Adapt_r & \triangleq &
\ifte{e}{\mupdate{\nm{r}}{\componente{\nm{v} }{0}{\mathsf{X}}}{\sigma}{\sigma}}
{\mupdate{\nm{r} }{\componente{\nm{r}_1 }{0}{\nmu{S'} }  \parallel \componente{\nm{r}_2 }{0}{\nmu{S''} } }{\sigma}{\mathcal{I}}} \quad\text{where:} \\
\nmu{S'}  \!\!& \!\!\triangleq \!\!&\!\!\nopen{a}{s}.\nopenr{b}{d}.\throw{d}{s}.\close{d} \\
\nmu{S''}  \!\!& \!\!\triangleq \!\!& \!\!\nopena{b}{e}.\catch{e}{s}.\inC{s}{u,p}.\select{s}{n_1.Q[s]}.\close{s}.\close{e} 
\end{eqnarray*}

%\bigskip

Adaptation 
for the current behavior at $r$ 
then depends on  $e$. \\ \smallskip

If $e$ reduces to true then behavior is \emphcolorb{relocated} to $v$. \\
Otherwise, behavior is discarded, and 
\emphcolor{replaced} with a delegation-based implementation.

}

\frame{
\frametitle{Consistency: Intuition}

A very simple scenario:
$$
Sys = (\nu \kappa)(\componente{client}{1}{Q_{\kappa}} \parallel \componente{server}{1}{S_{\kappa}}) \parallel \mupdate{server}{\componente{server}{0}{NewDef}}{}{}$$

We wouldn't like to adapt $server$ at this point. 

\pause
\bigskip

We would prefer to conclude any open sessions before adapting $server$, as in, e.g.:
$$
Sys \pired^* \equiv \componente{client}{0}{Q'_{\kappa}} \parallel \componente{server}{0}{S'_{\kappa}} \parallel \mupdate{server}{\componente{server}{0}{NewDef}}{}{}$$

}

%\frame{
%\frametitle{Example: A simple model of workflow adaptation (2)}
%Recall 
% $$
%\nm{W}_{i} \triangleq \componentbbig{\nm{w}_{i}^0}{\,  \emphcolor{\nmu{WL}_{i}} \parallel  \component{\nm{r}}{0}{}{\nmu{P}_{1}} \parallel  \component{\nm{t}}{0}{}{\nmu{P}_{2}} \,}
%$$
%Suppose $\emphcolor{\nmu{WL}_{i}}$ contains a \emphcolorb{reconfiguration policy} $Rec$ for $\nm{W}_{i}$: 
%%for location $\nm{r}_{}$.
%\begin{eqnarray*}
%Rec & \triangleq &
%\ifte{e}{\mupdate{\nm{r}}{\componente{\nm{v} }{0}{\mathsf{X}}}{\sigma}{\sigma}}
%{\mupdate{\nm{r} }{\componente{\nm{r}_1 }{0}{\nmu{S'} }  \parallel \componente{\nm{r}_2 }{0}{\nmu{S''} } }{\sigma}{\mathcal{I}}} \quad\text{where:} \\
%\nmu{S'}  \!\!& \!\!\triangleq \!\!&\!\!\nopen{a}{s}.\nopenr{b}{d}.\throw{d}{s}.\close{d} \\
%\nmu{S''}  \!\!& \!\!\triangleq \!\!& \!\!\nopena{b}{e}.\catch{e}{s}.\inC{s}{u,p}.\select{s}{n_1.Q[s]}.\close{s}.\close{e} \\
%\end{eqnarray*}
%
%\pause
%\bigskip
%Runtime reconfiguration then depends on the boolean $e$. \\ % evaluates to:
%If $e$ reduces to true then simply \emphcolorb{relocate} at $v$ the current behavior:
%$$
%\nm{W}_{i} \pired^* \componentbbig{\nm{w}_{i}^0}{\, \componente{\nm{v}}{0}{\nmu{P}_1}  \parallel \componente{\nm{t}}{0}{\nmu{P}_{2}}  \,}
%$$
%Otherwise, if $e$ evaluates to false then \emphcolor{replace} current behavior with the delegation-based implementation defined by $Rec$:
%\begin{equation*}
%\nm{W}_{i} \pired^* \componentbbig{\nm{w}_{i}^0}{\, \componente{\nm{r}_1}{0}{\nmu{S'}}  \parallel \componente{\nm{r}_2}{0}{\nmu{S''}}  \parallel \ \componente{\nm{t}}{0}{\nmu{P}_{2}}  \,} \label{eq:l}
%\end{equation*}
%%Thus, in a single step, 
%%the monolithic service $\nmu{P}_1$ will be replaced with a more flexible 
%%implementation in which $\nmu{P'} $ (located  at $\nm{r}_1$) first establishes a session and then \emph{delegates} it to $\nmu{P''} $ (located at $\nm{r}_2$).
%
%}

\frame{
\frametitle{Type System: Syntax}
We have deliberately aimed at retaining a type structure close to standard session types presentations. 

\smallskip

%Assuming a set of \emphcolor{basic types}, ranged over $\capab, \capab', \ldots$, we have:
$$
\begin{array}{lrl}
%\text{Basic types  } \capab & ::= & \mathsf{int} \sepr \mathsf{b ool} \sepr \dots ~~~ \\
\text{}\alpha, \alpha' & ::= & \epsilon  \!
		~\sepr~   !(\tilde{S}).\alpha 
		~\sepr~ ?(\tilde{S}).\alpha  
		~\sepr~   !(\alpha').\alpha 
		~\sepr~ ?(\alpha').\alpha \\
	%	&  \sepr& t ~\sepr~   \mu t.\alpha \\
	& \sepr & 	  \&\{n_1:\alpha_1, \dots,  n_k:\alpha_k \}   
		~\sepr~   \oplus\{n_1:\alpha_1, \dots , n_k:\alpha_k \}   \\ 
		& & \\
		\text{} S & ::= &  \mathsf{int} \sepr \mathsf{bool} \sepr \langle \alpha, \overline{\alpha} \rangle
%\text{Type Qualifiers  } \qua & ::= & \qual \sepr \quau  \! \\
%\text{}\omega &::=& \rho_\qua \sepr 	\bot 
\end{array}
$$
}



\frame{
\frametitle{Type System: Judgments}

\begin{block}{Type judgment}
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Delta}{\mathcal{I}}} $$
Under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\Delta$ and interface %(a collection of not yet open sessions) 
$\mathcal{I}$. 
\end{block}

\bi
\item Interfaces $\mathcal{I}$ are sequences of session types $\alpha$. 
\\ Available (declared) but not yet active sessions
%We also require a
\item Set~$\Delta$  collects information on already open sessions
\item $\Gamma$  maps expressions with basic types $\capab$. \\ It also records channels and sessions/sorts.
\item $\Theta$ %is a higher-order env.: it 
 maps process variables and locations to interfaces
\ei



}



\frame{
\frametitle{Type System: Key Typing Rules}
%We only present typing rules for adaptable and update processes; see~\cite{dGP13} for a full account.

Service declaration adds a typed description of the interface:
$$
\begin{array}{lc}
\rulename{t:Accept} &
 \cfrac{
\Gamma \vdash a: \langle \alpha , \overline{\alpha} \rangle \quad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{x:\alpha}{\,\mathcal{I}}} 
}{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P}{ \type{\emptyset}{\,\mathcal{I} \uplus a: \alpha}}} 
\end{array}
$$

\smallskip

We count open (but hidden) sessions via ``bracketing'':
$$
\begin{array}{lc}
\rulename{t:Cres} &
\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\Delta, \kappa^-:\alpha, \kappa^+:\overline{\alpha} }{ \mathcal{I}}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\kappa}{P}}{\type{\Delta}{ \mathcal{I}, \kappa^-:[\alpha], \kappa^+:[\overline{\alpha}]}}} 
\end{array}
$$

\smallskip

%Rule $\rulename{t:Loc}$ checks that the annotation for located processes corresponds to the number of open sessions:
Rules for adaptable and update processes:
$$
\begin{array}{lc}
\rulename{t:Loc} & \cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Delta}{\mathcal{I}}} \qquad h = \#\{k \mid k:\alpha \in \Delta \lor  k:[\alpha] \in \mathcal{I}\}}{\judgebis{\env{\Gamma}{\Theta}}{\componente{loc}{h}{P} }{ \type{\Delta}{\mathcal{I}}}} \\ \\
\rulename{t:Upd}   & 
\cfrac{\Theta \vdash loc:\mathcal{I}_1 \quad \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\mathcal{I}_1}}}{P}{\type{\emptyset}{ \mathcal{I}_2 }} \quad \mathcal{I}_1 \compat \mathcal{I}_2}{\judgebis{\env{\Gamma}{\Theta}}{\updated{loc}{X}{}{}{P}}{\type{\emptyset}{ \emptyset}}}
\end{array}
$$

 
}




\frame{
\frametitle{Consistency}

Some notation
\bi
%\item Process $P$ is said to be \emphcolor{communicating} over channel $k$
%if it sends (resp. receives) a value/session on $k$, if it makes a selection (resp. offers a choice), or if 
%it closes a session on $k$. 
%
%\item Two communicating processes are \emphcolor{dual} on session $k$ if they are complementary to each other
%%i.e., if one sends, the other receives on $c$; if one makes a selection, the other chooses; or if they are closing the same session $c$.
\item We write $Q_{\langle k \rangle}$ and $\overline{Q}_{\langle k \rangle}$ for dual comm. processes on $k$.

\item $\pired_r$ denotes a reduction originated from an update action
%an update action, i.e., a reduction inferred using rule $\rulename{r:Upd}$ 
%(possibly with the interplay of restriction/structural congruence rules).
%We say that %\begin{definition}[Consistency]\label{d:consist}%
\ei

A session on $k$ is \emphcolorb{consistent} in a process $P$ if,
for all $P', P''$ s.t. 
$$P \pired^{*} P' \equiv (\nu \tilde{u})\big (E\big[C[Q_{\langle k \rangle}] \parallel D[\overline{Q}_{\langle k \rangle}]\big] \big)$$
%where $R$ and $Q$ are dual communicating processes in that session, 
and $P' \pired_r P''$, then $\exists E', C', D'$ such that
$$P'' \equiv (\nu \tilde{u})\big (E'\big[C'[Q_{\langle k \rangle}] \parallel D'[\overline{Q}_{\langle k \rangle}]\big]\big)$$

\begin{block}{Main results}
\bi
\item Well-typedness is preserved by reduction (up to interfaces).
\item Well-typedness ensures every declared session is consistent.
\ei
\end{block}
}


%\frame{
%\frametitle{Con\-sist\-ency by Typing}
%\begin{corollary}\label{cor:cons}
%Suppose  
%$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Delta}{\mathcal{I}}} $
%is a well-typed process. \\
%Then every declared session $\rho$ % \in {\mathcal{I}}$ %that can be established along the evolution of $P$, we have that 
%is consistent. %, in the sense of Def.~\ref{d:consist}.
%\end{corollary}
%}

\section{Concluding Remarks}

\frame{
\frametitle{Concluding Remarks}

\str{Adaptable Processes}

\bi
\item A process calculi approach to express and reason about communicating systems which dynamically evolve at runtime
\item Promote a separation of concerns between actual behavior and its associated adaptation mechanisms
\item General enough to support variations, refinements, specializations
\ei

}

\frame{
\frametitle{Ongoing and Future Work}
Many exciting directions!
\bi
\item  Refine update actions with notions of \\
\begin{center}
subtyping / contracts / interface compatibility 
\end{center}
%(as in work by, e.g., Castagna et al)
\item Investigate stronger notions of correctness in the presence of adaptation (in particular, progress)
%\item  Cast adaptable processes in other session types disciplines \\ (in particular, Giunti and Vasconcelos's)
%\item Updates as an action declared in (and checked by) typing
\item Adaptable processes in a multi-party setting
\ei
}

\begin{frame}
%\progressbaroptions{titlepage=normal}

 \titlepage
\end{frame}

\end{document}

